abstract interpretation

theory A partial execution of a program which gains

information about its semantics (e.g. control structure,

flow of information) without performing all the calculations.

Abstract interpretation is typically used by compilers to

analyse programs in order to decide whether certain

optimisations or transformations are applicable.

The objects manipulated by the program (typically values and

functions) are represented by points in some domain. Each

abstract domain point represents some set of real

("concrete") values.

For example, we may take the abstract points "+", "0" and "-"

to represent positive, zero and negative numbers and then

define an abstract version of the multiplication operator, *#,

which operates on abstract values:

*# | + 0 -

---|------

+ | + 0 -

0 | 0 0 0

- | - 0 +

An interpretation is "safe" if the result of the abstract

operation is a safe approximation to the abstraction of the

concrete result. The meaning of "a safe approximation"

depends on how we are using the results of the analysis.

If, in our example, we assume that smaller values are safer

then the "safety condition" for our interpretation (#) is

a# *# b# #@= (a * b)#

where a# is the abstract version of a etc.

In general an interpretation is characterised by the domains

used to represent the basic types and the abstract values it

assigns to constants (where the constants of a language

include primitive functions such as *). The interpretation of

constructed types (such as user defined functions, sum types

and product types) and expressions can be derived

systematically from these basic domains and values.

A common use of abstract interpretation is strictnessanalysis.

See also standard interpretation.

(1994-11-08)